Inference at * 1 
Iof proof for Lemma sq stable iff:



1. P : 
2. Q : 
3. SqStable(P)
4. SqStable(Q)
  SqStable(P  Q) 

latex

 by InteriorProof ((((Repeat (Unfolds ``iff rev_implies`` 0)) 
CollapseTHEN (
CollapseTHEN (Backchain ``sq_stable__and sq_stable__implies``))) 
CollapseTHEN (
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
CollapseTHEN () inil_term))) 

latex

C.

Definitions	P  Q, P  Q, P  Q, t  T, , x:A. B(x)
Lemmas	sq stable implies, sq stable and